1. Field of the Invention
The present invention relates to a program synthesis system for generating a program by synthesizing an object described in an object-oriented language on the basis of a predetermined specification, e.g., a formal specification described in an algebraic specification description language.
2. Description of the Related Art
When an object described in an object-oriented language is generated on the basis of a given formal specification, the following methods are employed.
In one method, a given formal specification is detailed stepwise according to a predetermined procedure by positive intervention of man, and thereafter, an object is synthesized. In this method, however, since the program is generated by intervention of man, it is difficult to guarantee quality of the generated program. Furthermore, different programs may be generated depending on the degree or method of intervention of man. Therefore, it is difficult to generate a high-quality program unless the above-mentioned method is executed by a considerably skilled person.
A method of synthesizing an object by an automatic certification scheme has also been studied. However, the size of a program which can be generated is very small yet. Therefore, it is difficult to generate a program having a practical level size.
As described above, it is difficult to synthesize a high-quality program having a practical level size.
For the purpose of improving productivity of software, component conversion or re-utilization techniques of software have been proposed. However, the component conversion or re-utilization techniques of software suffer from the following problems, and requirements for high productivity cannot always be satisfied.
The conventional component conversion or re-utilization techniques of software suffer from the following problems. That is,
1) Since these techniques have no conversion knowledge for functionally decomposing given predetermined specifications, the specifications cannot be effectively functionally decomposed.
2) No efficient retrieval means for retrieving components having similar functions has been established.
3) No procedure for partially correcting a retrieved component has been established.
As described above, it is very difficult to synthesize a program on the basis of a given predetermined specification while assuring both high productivity and high quality.
As the reference associated with the present invention, Zohar Manna and Richard Waldinger, "The Logical Basis for Computer Programming; Vol. 2 Deductive Systems", ADDISON-WESLEY PUBLISHING COMPANY (1990) is known.